A, B, C:MsgA. A  C  B  C  A  B  C 

latex

Definitions

M1  M2, mk-ma, M1  M2, MsgA, Valtype(da;k), A & B, P & Q, left+right, strong-subtype(A;B), f  g, x:A. B(x), a:A fp B(a), S  T, S  T, union-deq(A;B;a;b), sumdeq(a;b), sum-deq(A;B;a;b), IdLnkDeq, product-deq(A;B;a;b), proddeq(a;b), prod-deq(A;B;a;b), AtomDeq, atom-deq-aux, NatDeq, <a,b>, nat-deq-aux, f(a), Prop, Atom, , {x:A| B(x) }, , AB, A, False, a<b, #$n, x:AB(x), x:AB(x), State(ds), type List, f(x)?z, locl(a), Top, 1of(t), IdDeq, Id, P  Q, Type, Void, KindDeq, rcv(l,tg), 2of(t), x. t(x), x:A. B(x), x.A(x), IdLnk, Knd, t  T

Lemmas

Knd wf, IdLnk wf, pi2 wf, rcv wf, Kind-deq wf, subtype-fpf-cap-void, Id wf, id-deq wf, pi1 wf, top wf, subtype-fpf-cap-top, locl wf, fpf-cap wf, subtype rel list, subtype rel function, subtype rel self, subtype rel dep function, ma-state wf, subtype rel product, strong-subtype-self, subtype-fpf3, fpf-trivial-subtype-top, idlnk-deq wf, product-deq wf, fpf-join-sub2, msga wf, ma-sub wf